df

2021-10-30 18:51:43 +01:00 · 2021-10-30 18:51:43 +01:00 · 6b97d4b790
commit 6b97d4b790
parent 4d5a2ded5a
2 changed files with 1 additions and 2 deletions
--- a/0Trinitarianism/Quest4Solutions.agda
+++ b/0Trinitarianism/Quest4Solutions.agda
@ -1,6 +1,6 @@
 module 0Trinitarianism.Quest4Solutions where

-open import Cubical.Foundations.Prelude using ( Level ; Type ; _≡_ ; J ; JRefl ; refl )
+open import Cubical.Foundations.Prelude using ( Level ; Type ; _≡_ ; J ; JRefl ; refl ; i1 ; i0 ; I)
 open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)

 infixr 30 _∙_
@ -184,7 +184,6 @@ endPtRefl {x = x} B = JRefl ((λ y p → B x → B y)) id
 endPt' : (B : A → Type) (p : x ≡ y) → B x → B y
 endPt' B p = pathToFun (Cubical.Foundations.Prelude.cong B p )

-
 --------------funExt---------------------

 funExt : (B : A → Type) (f g : (a : A) → B a) →
--- a/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai
+++ b/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai