Step * 1 of Lemma discrete-fun-bijection


1. Type
2. Type
3. a1 {() ⊢ _:(discr(A) ⟶ discr(B))}
4. a2 {() ⊢ _:(discr(A) ⟶ discr(B))}
5. discrete-fun(a1) discrete-fun(a2) ∈ {() ⊢ _:discr(A ⟶ B)}
⊢ a1 a2 ∈ {() ⊢ _:(discr(A) ⟶ discr(B))}
BY
(RenameVar `f' (-3) THEN RenameVar `g' (-2) THEN (CubicalTermEqual THEN Auto) THEN Fold `cubical-term-at` 0) }

1
1. Type
2. Type
3. {() ⊢ _:(discr(A) ⟶ discr(B))}
4. {() ⊢ _:(discr(A) ⟶ discr(B))}
5. discrete-fun(f) discrete-fun(g) ∈ {() ⊢ _:discr(A ⟶ B)}
6. fset(ℕ)
7. ()(I)
⊢ f(a) g(a) ∈ (discr(A) ⟶ discr(B))(a)


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  a1  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
4.  a2  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
5.  discrete-fun(a1)  =  discrete-fun(a2)
\mvdash{}  a1  =  a2


By


Latex:
(RenameVar  `f'  (-3)
  THEN  RenameVar  `g'  (-2)
  THEN  (CubicalTermEqual  THEN  Auto)
  THEN  Fold  `cubical-term-at`  0)




Home Index